*2(*2(x, y), z) -> *2(x, *2(y, z))
*2(+2(x, y), z) -> +2(*2(x, z), *2(y, z))
*2(x, +2(y, f1(z))) -> *2(g2(x, z), +2(y, y))
↳ QTRS
↳ DependencyPairsProof
*2(*2(x, y), z) -> *2(x, *2(y, z))
*2(+2(x, y), z) -> +2(*2(x, z), *2(y, z))
*2(x, +2(y, f1(z))) -> *2(g2(x, z), +2(y, y))
*12(+2(x, y), z) -> *12(x, z)
*12(*2(x, y), z) -> *12(y, z)
*12(+2(x, y), z) -> *12(y, z)
*12(x, +2(y, f1(z))) -> *12(g2(x, z), +2(y, y))
*12(*2(x, y), z) -> *12(x, *2(y, z))
*2(*2(x, y), z) -> *2(x, *2(y, z))
*2(+2(x, y), z) -> +2(*2(x, z), *2(y, z))
*2(x, +2(y, f1(z))) -> *2(g2(x, z), +2(y, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
*12(+2(x, y), z) -> *12(x, z)
*12(*2(x, y), z) -> *12(y, z)
*12(+2(x, y), z) -> *12(y, z)
*12(x, +2(y, f1(z))) -> *12(g2(x, z), +2(y, y))
*12(*2(x, y), z) -> *12(x, *2(y, z))
*2(*2(x, y), z) -> *2(x, *2(y, z))
*2(+2(x, y), z) -> +2(*2(x, z), *2(y, z))
*2(x, +2(y, f1(z))) -> *2(g2(x, z), +2(y, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
*12(x, +2(y, f1(z))) -> *12(g2(x, z), +2(y, y))
*2(*2(x, y), z) -> *2(x, *2(y, z))
*2(+2(x, y), z) -> +2(*2(x, z), *2(y, z))
*2(x, +2(y, f1(z))) -> *2(g2(x, z), +2(y, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
*12(+2(x, y), z) -> *12(x, z)
*12(*2(x, y), z) -> *12(y, z)
*12(+2(x, y), z) -> *12(y, z)
*12(*2(x, y), z) -> *12(x, *2(y, z))
*2(*2(x, y), z) -> *2(x, *2(y, z))
*2(+2(x, y), z) -> +2(*2(x, z), *2(y, z))
*2(x, +2(y, f1(z))) -> *2(g2(x, z), +2(y, y))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
*12(+2(x, y), z) -> *12(x, z)
*12(*2(x, y), z) -> *12(y, z)
*12(+2(x, y), z) -> *12(y, z)
*12(*2(x, y), z) -> *12(x, *2(y, z))
[+2, *2]
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
*2(*2(x, y), z) -> *2(x, *2(y, z))
*2(+2(x, y), z) -> +2(*2(x, z), *2(y, z))
*2(x, +2(y, f1(z))) -> *2(g2(x, z), +2(y, y))